$\forall$${\it es}$:ES, $e$:E, $P$:(\{$a$:E$\mid$ loc($a$) = loc($e$) $\in$ Id\} $\rightarrow\mathbb{B}$).
\\[0ex]$\forall$${\it e'}$$\leq$$e$.$P$(${\it e'}$) = $P$($e$) $\vee$ $\exists$${\it e'}$$\leq$$e$.($\neg$($P$(${\it e'}$) = $P$($e$))) \& $\forall$${\it e''}$$\in$(${\it e'}$,$e$].$P$(${\it e''}$) = $P$($e$)